PRISM
=====
Version: 4.5.dev
Date: Sun Mar 15 03:29:19 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 firewire-pta.prism firewire-pta.props --property deadline -const 'delay=30,T=5000'
Parsing model file "firewire-pta.prism"...
Type: PTA
Modules: wire12 node1 wire21 node2
Variables: w12 y1 y2 x1 s1 w21 z1 z2 x2 s2
Parsing properties file "firewire-pta.props"...
2 properties:
(1) "deadline": Pmin=? [ F<=T "done" ]
(2) "eventually": Pmin=? [ F "done" ]
---------------------------------------------------------------------
Model checking: "deadline": Pmin=? [ F<=T "done" ]
Model constants: delay=30
Property constants: T=5000
Building PTA...
PTA: 6 clocks, 65 locations, 127 transitions
Target (s1=8&s2=7|s1=7&s2=8) satisfied by 4 locations.
Modifying PTA to encode time bound from property...
New PTA: 7 clocks, 66 locations, 135 transitions
Building initial STPG...
Building forwards reachability graph... 3469 states
Graph constructed in 0.193 secs.
Graph: 3469 symbolic states (1 initial, 130 target)
Model checking STPG...
STPG model checked in 0.28 secs.
2634/3469 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
42 refineable states.
Refinement 1...
42 states successfully refined in 0.217 secs.
180+0=180 states of STPG rebuilt in 0.0 secs.
New STPG has 3511 states.
Model checking STPG...
STPG model checked in 0.155 secs.
2718/3511 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
96 refineable states.
Refinement 2...
96 states successfully refined in 0.359 secs.
288+0=288 states of STPG rebuilt in 0.0 secs.
New STPG has 3607 states.
Model checking STPG...
STPG model checked in 0.175 secs.
2910/3607 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
36 refineable states.
Refinement 3...
36 states successfully refined in 0.094 secs.
132+0=132 states of STPG rebuilt in 0.0 secs.
New STPG has 3643 states.
Model checking STPG...
STPG model checked in 0.093 secs.
2982/3643 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
60 refineable states.
Refinement 4...
60 states successfully refined in 0.119 secs.
180+0=180 states of STPG rebuilt in 0.0 secs.
New STPG has 3703 states.
Model checking STPG...
STPG model checked in 0.106 secs.
3102/3703 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
60 refineable states.
Refinement 5...
60 states successfully refined in 0.114 secs.
162+0=162 states of STPG rebuilt in 0.0 secs.
New STPG has 3763 states.
Model checking STPG...
STPG model checked in 0.075 secs.
3222/3763 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 1.0
42 refineable states.
Refinement 6...
42 states successfully refined in 0.072 secs.
108+0=108 states of STPG rebuilt in 0.0 secs.
New STPG has 3805 states.
Model checking STPG...
STPG model checked in 0.069 secs.
3306/3805 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
24 refineable states.
Refinement 7...
24 states successfully refined in 0.043 secs.
75+0=75 states of STPG rebuilt in 0.0 secs.
New STPG has 3829 states.
Model checking STPG...
STPG model checked in 0.067 secs.
3354/3829 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
27 refineable states.
Refinement 8...
27 states successfully refined in 0.071 secs.
66+0=66 states of STPG rebuilt in 0.0 secs.
New STPG has 3856 states.
Model checking STPG...
STPG model checked in 0.064 secs.
3408/3856 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
12 refineable states.
Refinement 9...
12 states successfully refined in 0.042 secs.
42+0=42 states of STPG rebuilt in 0.0 secs.
New STPG has 3880 states.
Model checking STPG...
STPG model checked in 0.073 secs.
3444/3880 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
6 refineable states.
Refinement 10...
6 states successfully refined in 0.089 secs.
58+0=58 states of STPG rebuilt in 0.0 secs.
New STPG has 3892 states.
Model checking STPG...
STPG model checked in 0.072 secs.
3462/3892 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.
Refinement 11...
40 states successfully refined in 0.283 secs.
160+0=160 states of STPG rebuilt in 0.0 secs.
New STPG has 3972 states.
Model checking STPG...
STPG model checked in 0.071 secs.
3582/3972 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.
Refinement 12...
40 states successfully refined in 0.319 secs.
144+0=144 states of STPG rebuilt in 0.0 secs.
New STPG has 4036 states.
Model checking STPG...
STPG model checked in 0.067 secs.
3686/4036 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
40 refineable states.
Refinement 13...
40 states successfully refined in 0.148 secs.
132+0=132 states of STPG rebuilt in 0.0 secs.
New STPG has 4100 states.
Model checking STPG...
STPG model checked in 0.075 secs.
3790/4100 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.5
28 refineable states.
Refinement 14...
28 states successfully refined in 0.118 secs.
88+0=88 states of STPG rebuilt in 0.0 secs.
New STPG has 4144 states.
Model checking STPG...
STPG model checked in 0.074 secs.
3862/4144 states converged.
Diff across 1 initial state: 0.056640625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.908203125
Max diff over all states: 0.25
16 refineable states.
Refinement 15...
16 states successfully refined in 0.066 secs.
60+0=60 states of STPG rebuilt in 0.0 secs.
New STPG has 4168 states.
Model checking STPG...
STPG model checked in 0.076 secs.
3902/4168 states converged.
Diff across 1 initial state: 0.041015625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.892578125
Max diff over all states: 0.25
20 refineable states.
Refinement 16...
20 states successfully refined in 0.074 secs.
68+0=68 states of STPG rebuilt in 0.0 secs.
New STPG has 4200 states.
Model checking STPG...
STPG model checked in 0.084 secs.
3950/4200 states converged.
Diff across 1 initial state: 0.041015625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.892578125
Max diff over all states: 0.15625
16 refineable states.
Refinement 17...
16 states successfully refined in 0.054 secs.
52+0=52 states of STPG rebuilt in 0.0 secs.
New STPG has 4228 states.
Model checking STPG...
STPG model checked in 0.074 secs.
3974/4228 states converged.
Diff across 1 initial state: 0.025390625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.876953125
Max diff over all states: 0.15625
8 refineable states.
Refinement 18...
6 states successfully refined in 0.092 secs.
58+0=58 states of STPG rebuilt in 0.0 secs.
New STPG has 4240 states.
Model checking STPG...
STPG model checked in 0.074 secs.
3986/4240 states converged.
Diff across 1 initial state: 0.025390625
Lower/upper bounds for 1 initial state: 0.8515625 - 0.876953125
Max diff over all states: 0.15625
44 refineable states.
Refinement 19...
40 states successfully refined in 0.236 secs.
160+0=160 states of STPG rebuilt in 0.0 secs.
New STPG has 4320 states.
Model checking STPG...
STPG model checked in 0.077 secs.
4175/4320 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
26 refineable states.
Refinement 20...
10 states successfully refined in 0.077 secs.
36+0=36 states of STPG rebuilt in 0.0 secs.
New STPG has 4336 states.
Model checking STPG...
STPG model checked in 0.086 secs.
4201/4336 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
26 refineable states.
Refinement 21...
10 states successfully refined in 0.038 secs.
33+0=33 states of STPG rebuilt in 0.0 secs.
New STPG has 4352 states.
Model checking STPG...
STPG model checked in 0.155 secs.
4227/4352 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.125
23 refineable states.
Refinement 22...
7 states successfully refined in 0.037 secs.
22+0=22 states of STPG rebuilt in 0.0 secs.
New STPG has 4363 states.
Model checking STPG...
STPG model checked in 0.175 secs.
4245/4363 states converged.
Diff across 1 initial state: 0.001953125
Lower/upper bounds for 1 initial state: 0.8515625 - 0.853515625
Max diff over all states: 0.0625
20 refineable states.
Refinement 23...
4 states successfully refined in 0.018 secs.
16+0=16 states of STPG rebuilt in 0.0 secs.
New STPG has 4369 states.
Model checking STPG...
STPG model checked in 0.113 secs.
4332/4369 states converged.
Diff across 1 initial state: 0.0
Lower/upper bounds for 1 initial state: 0.8515625 - 0.8515625
Initial STPG: 3469 states (1 initial), 4982 transitions, 4620 choices, 3423 choice sets, p1max/avg = 3/0.99, p2max/avg = 2/1.35
Final STPG: 4369 states (1 initial), 8212 transitions, 7674 choices, 4756 choice sets, p1max/avg = 7/1.09, p2max/avg = 6/1.61
Terminated after 23 refinements in 6.20 secs.
Abstraction-refinement time breakdown:
* 0.94 secs (15.2%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (23 x avg 0.00 secs)
* 2.43 secs (39.2%) = model checking STPG (24 x avg 0.10 secs) (lb=46.1%) (prob0=20.5%) (pre=92.3%) (iters=964)
* 2.78 secs (44.8%) = refinement (23 x avg 0.12 secs)
Final diff across 1 initial state: 0.0
Final lower/upper bounds for 1 initial state: 0.8515625 - 0.8515625
Model checking completed in 6.398 secs.
Result (minimum probability): 0.8515625
Overall running time: 6.936 seconds.